\begin{figure}[H]
\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Require} \coqdockw{Import} \coqexternalref{}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Arith.EqNat}{\coqdoclibrary{Arith.EqNat}}.\coqdoceol
\coqdocnoindent
\coqdockw{Set Implicit Arguments}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Module} \coqdockw{Type} \coqdef{Lenguaje.ITipos}{ITipos}{\coqdocmodule{ITipos}}.\coqdoceol
\coqdocemptyline
\end{coqdoccode}
\textit{(* Tipos de datos *)}\\
\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Parameter} \coqdef{Lenguaje.ITipos.Bool}{Bool}{\coqdocaxiom{Bool}}    : \coqdockw{Set}.\coqdoceol
\coqdocnoindent
\coqdockw{Parameter} \coqdef{Lenguaje.ITipos.Integer}{Integer}{\coqdocaxiom{Integer}} : \coqdockw{Set}.\coqdoceol
\coqdocnoindent
\coqdockw{Parameter} \coqdef{Lenguaje.ITipos.Byte}{Byte}{\coqdocaxiom{Byte}}    : \coqdockw{Set}.\coqdoceol
\coqdocnoindent
\coqdockw{Parameter} \coqdef{Lenguaje.ITipos.Matrix}{Matrix}{\coqdocaxiom{Matrix}}  : \coqdockw{Set} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqdockw{Set}.\coqdoceol
\coqdocemptyline
\end{coqdoccode}
\textit{(* Constantes *)}\\
\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.TRUE}{TRUE}{\coqdocvariable{TRUE}}  : \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.FALSE}{FALSE}{\coqdocvariable{FALSE}} : \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.ONE}{ONE}{\coqdocvariable{ONE}} : \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.ZERO}{ZERO}{\coqdocvariable{ZERO}} : \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}}.\coqdoceol
\coqdocemptyline
\end{coqdoccode}
\textit{(* Operaciones sobre Bool *)}\\
\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.bool not}{bool\_not}{\coqdocvariable{bool\_not}} : \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.bool and}{bool\_and}{\coqdocvariable{bool\_and}} : \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.bool or}{bool\_or}{\coqdocvariable{bool\_or}}  : \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}}.\coqdoceol
\coqdocemptyline
\end{coqdoccode}
\textit{(* Operaciones sobre Integer *)}\\
\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.int plus}{int\_plus}{\coqdocvariable{int\_plus}}   : \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.int minus}{int\_minus}{\coqdocvariable{int\_minus}}  : \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.int mult}{int\_mult}{\coqdocvariable{int\_mult}}   : \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.int div}{int\_div}{\coqdocvariable{int\_div}}    : \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.int modulo}{int\_modulo}{\coqdocvariable{int\_modulo}} : \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.int eq}{int\_eq}{\coqdocvariable{int\_eq}}     : \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.int lt}{int\_lt}{\coqdocvariable{int\_lt}}     : \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.int le}{int\_le}{\coqdocvariable{int\_le}}     : \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.int gt}{int\_gt}{\coqdocvariable{int\_gt}}     : \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.int ge}{int\_ge}{\coqdocvariable{int\_ge}}     : \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}}.\coqdoceol
\coqdocemptyline
\end{coqdoccode}
\textit{(* Operaciones sobre Byte *)}\\
\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.byte xor}{byte\_xor}{\coqdocvariable{byte\_xor}} : \coqref{Lenguaje.ITipos.Byte}{\coqdocaxiom{Byte}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Byte}{\coqdocaxiom{Byte}}   \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Byte}{\coqdocaxiom{Byte}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.byte shl}{byte\_shl}{\coqdocvariable{byte\_shl}} : \coqref{Lenguaje.ITipos.Byte}{\coqdocaxiom{Byte}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Byte}{\coqdocaxiom{Byte}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.byte shr}{byte\_shr}{\coqdocvariable{byte\_shr}} : \coqref{Lenguaje.ITipos.Byte}{\coqdocaxiom{Byte}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Byte}{\coqdocaxiom{Byte}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.byte and}{byte\_and}{\coqdocvariable{byte\_and}} : \coqref{Lenguaje.ITipos.Byte}{\coqdocaxiom{Byte}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Byte}{\coqdocaxiom{Byte}}   \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Byte}{\coqdocaxiom{Byte}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.byte gt}{byte\_gt}{\coqdocvariable{byte\_gt}}  : \coqref{Lenguaje.ITipos.Byte}{\coqdocaxiom{Byte}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Byte}{\coqdocaxiom{Byte}}   \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.byte eq}{byte\_eq}{\coqdocvariable{byte\_eq}}  : \coqref{Lenguaje.ITipos.Byte}{\coqdocaxiom{Byte}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Byte}{\coqdocaxiom{Byte}}   \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Bool}{\coqdocaxiom{Bool}}.\coqdoceol
\coqdocemptyline
\end{coqdoccode}
\textit{(* Operaciones sobre Matrix *)}\\
\begin{coqdoccode}
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.matrix get}{matrix\_get}{\coqdocvariable{matrix\_get}} : \coqdockw{\ensuremath{\forall}} \coqdocvar{A} \coqdocvar{m} \coqdocvar{n}, \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Matrix}{\coqdocaxiom{Matrix}} \coqdocvariable{A} \coqdocvariable{m} \coqdocvariable{n} \ensuremath{\rightarrow} \coqexternalref{option}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocinductive{option}} \coqdocvariable{A}.\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.matrix set}{matrix\_set}{\coqdocvariable{matrix\_set}} : \coqdockw{\ensuremath{\forall}} \coqdocvar{A} \coqdocvar{m} \coqdocvar{n}, \coqref{Lenguaje.ITipos.Matrix}{\coqdocaxiom{Matrix}} \coqdocvariable{A} \coqdocvariable{m} \coqdocvariable{n} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqref{Lenguaje.ITipos.Integer}{\coqdocaxiom{Integer}} \ensuremath{\rightarrow} \coqdocvariable{A} \ensuremath{\rightarrow} \coqexternalref{option}{http://coq.inria.fr/distrib/8.4pl3/stdlib/Coq.Init.Datatypes}{\coqdocinductive{option}} (\coqref{Lenguaje.ITipos.Matrix}{\coqdocaxiom{Matrix}} \coqdocvariable{A} \coqdocvariable{m} \coqdocvariable{n}).\coqdoceol
\coqdocnoindent
\coqdockw{Variable} \coqdef{Lenguaje.ITipos.matrix zero}{matrix\_zero}{\coqdocvariable{matrix\_zero}} : \coqdockw{\ensuremath{\forall}} (\coqdocvar{A}:\coqdockw{Set})(\coqdocvar{a}:\coqdocvariable{A}) \coqdocvar{m} \coqdocvar{n}, \coqref{Lenguaje.ITipos.Matrix}{\coqdocaxiom{Matrix}} \coqdocvariable{A} \coqdocvariable{m} \coqdocvariable{n}.\coqdoceol
\coqdocemptyline
\coqdocnoindent
\coqdockw{End} \coqref{Lenguaje}{\coqdocmodule{ITipos}}.\coqdoceol
\end{coqdoccode}
\caption{Módulo de definición de tipos} \label{module:itypes}
\end{figure}
